package no.uio.ifi.cop.prover.simple;

import java.util.ArrayList;
import java.util.HashSet;

import no.uio.ifi.cop.prover.RuleMatcher;

import no.uio.ifi.cop.common.Log;
import no.uio.ifi.cop.cl.Axiom;
import no.uio.ifi.cop.cl.Term;
import no.uio.ifi.cop.cl.Conjunction;
import no.uio.ifi.cop.cl.Predicate;
import no.uio.ifi.cop.cl.Substitution;

/**
 * This class holds an Axiom and all its matching terms.
 *
 * 
 * @version 1.0
 * @author  bjarneh@ifi.uio.no
 */

public final class SimpleRuleMatcher extends RuleMatcher implements Cloneable{

    // every element gets its own id, and we use this to generate them..
    private static int counter = 1;

    HashSet<String> cache;

    boolean stopped;
    int length;
    // generics and arrays don't mix, so this funky
    // hybrid becomes the result. an array of 
    // ArrayList<Substitution> is what we want..
    private ArrayList<ArrayList<Substitution>> matches;
    int[] current;
    Term[] lhs;


    public SimpleRuleMatcher(Axiom ax){
        this( counter++, ax );
    }

    public SimpleRuleMatcher(int ID, Axiom ax){

        setId( ID );
        setAxiom( ax );

        length   = ax.getLHS().length(); 
        current  = new int[length];
        matches  = new ArrayList<ArrayList<Substitution>>(length);
        for( int i = 0; i < length; i++ ){
            matches.add( new ArrayList<Substitution>(20) );
            current[i]  = 0;
        }

        lhs = new Term[ length ];

        int i = 0;
        for( Term t : ax.getLHS() ){
            lhs[i++] = t;
        }

        cache = new HashSet<String>();

        stopped = false;
    }


    protected void stop(){
        stopped = true;
    }

    public Substitution getNextMatch(boolean cacheFind){

        Substitution subst;

        if( possible() ){
            
            do{
                subst = join();

                if( subst != null && ! inCache() ){
                    if( cacheFind ){
                        cacheCurrent();
                        advance();
                    }
                    return subst;   
                }

            }while( (! stopped) && advance() );

        }else{
            reset();
        }

        return null;
    }

    private boolean inCache(){
        return cache.contains( cacheEntryToString() );
    }

    private String cacheEntryToString(){
        StringBuilder sb = new StringBuilder();
        for( int i = 0; i < length; i++ ){
            sb.append(current[i]);
        }
        return sb.toString();
    }

    private void cacheCurrent(){
        cache.add( cacheEntryToString() );
    }

    private Substitution join(){

        Substitution one, two;
        one = matches.get(0).get( current[0] );

        for( int i = 1; i < length; i++ ){

            two = matches.get( i ).get( current[ i ] );
            one = two.join( one );

            if( one == null ){
                return null;
            }
        }

        return one;
    }

    private boolean possible(){
        for( int i = 0; i < length; i++ ){
            if( ! ( current[i] < matches.get(i).size() ) ){
                return false;
            }
        }
        return true;
    }

    protected boolean advance(){
        int max = length - 1;
        for( int i = 0; i < max; i++ ){
            if( current[i] < matches.get(i).size() - 1 ){
                current[i]++;
                return true;
            }else{
                current[i] = 0;
            }
        }

        if( current[max] < matches.get(max).size() - 1){
            current[max]++;
            return true;
        }

        return false;
    }

    protected void reset(){
        for( int i = 0; i < length; i++ ){
            current[i] = 0;
        }
    }

    public void match( Predicate p ){

        Substitution subst;

        for( int i = 0; i < length; i++ ){
            subst = new Substitution();
            if( lhs[i].match( subst, p ) ){
                Log.debug(" match: [ %s  <-  %s ]", lhs[i], p);
                matches.get(i).add( subst );
            }
        }
    }

    public int applications(){
        return cache.size();
    }

    // make shallow clone
    public SimpleRuleMatcher clone(){

        SimpleRuleMatcher fresh = new SimpleRuleMatcher( getId(), getAxiom() );

        ArrayList<Substitution> tmp;

        for( int i = 0; i < length; i++ ){
            tmp = matches.get( i );
            for( Substitution subst : tmp ){
                fresh.addSubstitution( i, subst );
            }
            fresh.addCurrent( i, current[i] );
        }

        for( String entry : cache ){
            fresh.addCacheEntry( entry );
        }

        return fresh;
    }

    protected void addCurrent( int where, int value ){
        current[ where ] = value;
    }

    protected void addSubstitution( int i, Substitution subst ){
        matches.get(i).add( subst );
    }

    protected void addCacheEntry( String entry ){
        cache.add( entry );
    }


    public String toString(){
        ArrayList<Substitution> tmp;
        StringBuilder sb = new StringBuilder();
        sb.append("@SimpleRuleMatcher\n");
        sb.append( getAxiom().toString() ).append("\n");
        for( int i = 0; i < length; i++ ){
            sb.append( lhs[i] ).append(": ");
            tmp = matches.get( i );
            for( Substitution subst : tmp ){
                sb.append( subst ).append(" | ");
            }
            sb.append("\n");
        }
        sb.append("[");
        for( int i = 0; i < length; i++ ){
            sb.append(String.format(" %d",current[i]));
        }
        sb.append(" ]\n");
        return sb.toString();
    }

}
